\begin{tabbing}
basic
\\[0ex]IsBilinear($A$;$B$;$C$;${\it +a}$;${\it +b}$;${\it +c}$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$a_{1}$:$A$, $a_{2}$:$A$, $b$:$B$. (($a_{1}$ ${\it +a}$ $a_{2}$) $f$ $b$) = (($a_{1}$ $f$ $b$) ${\it +c}$ ($a_{2}$ $f$ $b$)) $\in$ $C$)\+
\\[0ex]\& ($\forall$$a$:$A$. $\forall$$b_{1}$:$B$, $b_{2}$:$B$. ($a$ $f$ ($b_{1}$ ${\it +b}$ $b_{2}$)) = (($a$ $f$ $b_{1}$) ${\it +c}$ ($a$ $f$ $b_{2}$)) $\in$ $C$)
\-
\end{tabbing}